#include <string.h>
#include "mc.h"
#include <string.h>
#include "mhash.h"
#include "propositional_symbol.h"
#include "ltl2ba_adapter.h"
#include "error.h"
#include "task.h"
#include "dumper.h"
#include "delta_state.h"

#ifdef PROFILE
#include "runtime_status.h"
#endif

enum MC_ERRORNO {
  MC_ERR_NC_ENV,
  MC_ERR_PROP_ENV,
  MC_NC_OPEN_ERROR,
  MC_NC_LOAD_ERROR,
  MC_PROP_OPEN_ERROR,
  MC_PROP_LOAD_ERROR,
};
  
/* 状態IDが本来不必要な場合に使用する状態ID */
#define DEFAULT_STATE_ID 0

/* 訪問済みノードが格納される */
st_table *States;
/* 展開されたシステムの状態が格納される */
ExpandedList expanded;

/* 非決定的実行で用いるフラグ集合 */
McFlags mc_flags;
MCData mc_data;


static BOOL expand_inner(LmnMembrane *cur_mem, BOOL *must_be_activated);
static ExpandedList expand2(LmnMembrane *cur_mem);
static void dfs_expand(State *state,
                       int depth,
                       McState pred,
                       StateTransition transition,
                       int i_succ);
static void print_state(LmnMembrane *mem, McState mc_state);

/* フラグ集合を初期化する(c.f. mc.h) */
void init_mc_flags(void)
{
  mc_flags.nd_exec = FALSE;
  mc_flags.system_rule_committed = FALSE;
  mc_flags.system_rule_proceeded = FALSE;
  mc_flags.property_rule = FALSE;
  mc_flags.reacting_transition = FALSE;
  mc_flags.commit_count = 0;
}

McState visited_state(StateTable states, McState state)
{
  st_data_t visited;

  if (st_lookup(states, (st_data_t)state, &visited)) return (McState)visited;
  else return NULL;
}

void add_new_state(StateTable states, McState state)
{
  st_add_direct(states, (st_data_t)state, (st_data_t)state);
}

/**
 * コンストラクタ
 */
State *state_make_with_hash(LmnMembrane *mem,
                            unsigned long hash,
                            BYTE state_name,
                            lmn_interned_str rule) {
  State *new = LMN_MALLOC(State);
  new->mem = mem;
  new->state_name = state_name;
  new->flags = 0x00U;
  /* successorの記憶域をゼロクリアする */
  vec_init(&new->successor, 1);
  /* ハッシュ値はあらかじめ計算しておく */
  new->hash = hash;
  new->rule_name = rule;

#ifdef PROFILE
  status_add_explicit_state_space(sizeof(State));
#endif
  return new;
}

/**
 * コンストラクタ
 */
State *state_make(LmnMembrane *mem, BYTE state_name, lmn_interned_str rule) {
  State *s = state_make_with_hash(mem, mhash(mem), state_name, rule);
  return s;
}

/**
 * コンストラクタ
 */
State *state_make_for_nd(LmnMembrane *mem, lmn_interned_str rule) {
  return state_make(mem, DEFAULT_STATE_ID, rule);
}

/**
 * 記憶域sの最初のnバイトがゼロであることを確認する
 */
static inline BOOL mem_is_zero(const void *s, size_t n) {
  const unsigned char *p = (const unsigned char *)s;
  while (n-- > 0 ) {
    if(*p != 0x00U) return FALSE;
    p++;
  }
  return TRUE;
}

inline void state_succ_init(State *s, int init_size) {
  vec_resize(&s->successor, init_size, 1);
}

inline void state_set_successor(State *s, int i, void *succ)
{
  vec_set(&s->successor, i, (vec_data_t)succ);
}

inline McState state_get_successor(State *s, int i)
{
  return (McState)vec_get(&s->successor, i);
}

unsigned int state_successor_num(State *s)
{
  return vec_num(&s->successor);
}

/**
 * デストラクタ
 */
void state_free(State *s) {
  lmn_mem_drop(s->mem);
  lmn_mem_free(s->mem);
  state_free_without_mem(s);
}

void state_free_without_mem(State *s)
{
  if (!mem_is_zero(&s->successor, sizeof(Vector))) {
    vec_destroy(&s->successor);
  }
  LMN_FREE(s);

#ifdef PROFILE
  status_remove_explicit_state_space(sizeof(State));
#endif
}

inline long state_hash(void *s) {
  return
    IS_EXPLICIT_STATE(s) ?
    ((State *)s)->hash : ((DeltaState)s)->hash;
}

BYTE state_property_state(State *state)
{
  return state->state_name;
}

/**
 * 引数としてあたえられたStateが等しいかどうかを判定する
 * ハッシュ値が等しい場合は同型判定を行う
 */
static int state_equals(HashKeyType k1, HashKeyType k2) {
  int r;
  State *s1; 
  State *s2; 
  BOOL s1_new, s2_new;
  
  s1_new = reconstitute((void *)k1, &s1);
  s2_new = reconstitute((void *)k2, &s2);

  r =
    s1->state_name == s2->state_name &&
    state_hash(s1) == state_hash(s2) &&
    lmn_mem_equals(s1->mem, s2->mem);

  if (s1_new) state_free(s1);
  if (s2_new) state_free(s2);

  return r;
}

/**
 * 与えられた2つの状態が互いに異なっていれば真を、逆に等しい場合は偽を返す
 */
int state_cmp(HashKeyType s1, HashKeyType s2) {
  return !state_equals(s1, s2);
}

static void print_state(LmnMembrane *mem, McState mc_state)
{
  fprintf(stdout, "%lu::", state_id(mc_state)); /* dump src state's ID */
  lmn_dump_cell(mem); /* dump src state's global root membrane */
}

void print_successor(McState mc_state)
{
  int i;
  const int n = mc_state_successor_num(mc_state);

  fprintf(stdout, "%lu->", state_id(mc_state));
  for (i = 0; i < n; i++) {
    if (i>0) fprintf(stdout, " ");
    fprintf(stdout, "%lu", state_id(mc_state_get_successor(mc_state, i)));
  }
  fprintf(stdout, "\n");
}

/**
 * 膜スタックの代替品
 * 自身を含めた全ての先祖膜を起こす
 */
inline void activate_ancestors(LmnMembrane *mem) {
  LmnMembrane *cur;
  for (cur=mem; cur; cur=cur->parent) {
    cur->is_activated = TRUE;
  }
}

ExpandedList expanded_make()
{
  return vec_make(64);
}

void expanded_free(ExpandedList el)
{
  vec_free(el);
}

void expanded_clear(ExpandedList el)
{
  unsigned int i;

  for (i = 0; i < vec_num(el); i++) {
    LMN_FREE((ExpandedState)vec_get(el, i));
  }
  vec_clear(el);
}

unsigned int expanded_num(ExpandedList el)
{
  return vec_num(el);
}

ExpandedState expanded_get(ExpandedList el, int i)
{
  return (ExpandedState)vec_get(el, i);
}

void expanded_add(ExpandedList el, ExpandedState es)
{
  vec_push(el, (vec_data_t)es);
}

ExpandedState expanded_state_make(State *state, StateTransition transition)
{
  struct ExpandedState *es = LMN_MALLOC(struct ExpandedState);
  es->state = state;
  es->transition = transition;
  return es;
}

void expanded_state_free(ExpandedState es)
{
  LMN_FREE(es);
}

/* 成功ならば0, そうでないならば0以外を返す */
int mc_load_property(Automata *a, PVector *prop_defs)
{
  FILE *nc_fp, *prop_fp;
  int r;

  *a = NULL;
  *prop_defs = NULL;
  nc_fp = prop_fp = NULL;

  if (lmn_env.ltl_exp) {
    nc_fp = ltl2ba_str(lmn_env.ltl_exp);
  } else {
    if (!lmn_env.automata_file) goto NC_ENV;
    if (!(nc_fp = fopen(lmn_env.automata_file, "r"))) goto NC_OPEN_ERROR;
  }
  if (never_claim_load(nc_fp, a)) goto NC_LOAD_ERROR;
  
  if (!lmn_env.propositional_symbol) goto PROP_ENV;
  if (!(prop_fp = fopen(lmn_env.propositional_symbol, "r"))) goto PROP_OPEN_ERROR;
  if (propsym_load_file(prop_fp, *a, prop_defs)) goto PROP_LOAD_ERROR;

  r = 0;
  goto RET;
  
NC_ENV: r = MC_ERR_NC_ENV; goto FINALLY;
PROP_ENV: r = MC_ERR_PROP_ENV; goto FINALLY;
NC_OPEN_ERROR: r = MC_NC_OPEN_ERROR; goto FINALLY;
NC_LOAD_ERROR:
  {
    char c;
    rewind(nc_fp);
    while ((c = fgetc(nc_fp)) != EOF) {
      fputc(c, stderr);
    }
    r = MC_NC_LOAD_ERROR;
    goto FINALLY;
  }
PROP_OPEN_ERROR: r = MC_PROP_OPEN_ERROR; goto FINALLY;
PROP_LOAD_ERROR: r = MC_PROP_LOAD_ERROR; goto FINALLY;

FINALLY:
  LMN_FREE(*a);
  LMN_FREE(*prop_defs);

 RET:
  if (prop_fp) fclose(prop_fp);
  if (nc_fp) fclose(nc_fp);
  return r;
}

void mc_explain_error(int error_id)
{
  lmn_report(mc_error_msg(error_id));
}

char *mc_error_msg(int error_id)
{
  switch (error_id) {
  case MC_ERR_NC_ENV:
    return "specify never claim file";
  case MC_ERR_PROP_ENV:
    return "specify propositional symbol definition file";
  case MC_NC_OPEN_ERROR:
    return "cannot open never claim file";
  case  MC_NC_LOAD_ERROR:
    return "error while parsing never claim file";
  case MC_PROP_OPEN_ERROR:
    return "cannot open propositional symbol definition file";
  case MC_PROP_LOAD_ERROR:
    return "error while parsing propositional symbol definition file";
  default:
    lmn_fatal("implementation error\n");
    return NULL;
  }
}

void nd_exec(State *init_state)
{
  dfs_expand(init_state,
             0,
             NULL,
             state_transition_make_null(),
             -1);
}

/*
 * 深さ優先で全実行経路を表示する．
 * 差分状態による最適化を行っている.
 */
static void dfs_expand(State *state,
                       int depth,
                       McState pred,
                       StateTransition transition,
                       int i_succ)
{
  void *visited;

  if ((visited = visited_state(States, state)) != NULL) { /* already visited */
    mc_state_set_successor(pred, i_succ, visited);
    state_free(state);
  }
  else { /* first visit */
    McState new_state;
    unsigned int i;
    unsigned successor_num;
    ExpandedList el;
    const BOOL is_explicit = (depth%explicit_state_delta) == 0;
    
    el = expand2(state->mem);
    successor_num = expanded_num(el);
    /* 状態空間に保存する用の状態を生成 */
    if (is_explicit) new_state = state;
    else new_state = dstate_make(pred, transition, state);
    mc_state_init_successor(new_state, successor_num);
    if (pred) /* predはstateが初期状態の時にNULL */
      mc_state_set_successor(pred, i_succ, new_state);
    print_state(state->mem, new_state);
    if (!is_explicit) state_free(state);
    add_new_state(States, new_state);

    for (i = 0; i < successor_num; i++) {
      ExpandedState es = expanded_get(el, i);
      State *next_state;
      
      if (es->state) {
        next_state = es->state;
      } else {
        /* 明示的な状態で展開されなかった.
           predと遷移から状態を復元する */
        LmnMembrane *pre_mem;

        if (is_explicit) pre_mem = lmn_mem_copy(((State *)new_state)->mem);
        else reconstitute_mem(new_state, &pre_mem);

        next_state = state_make_for_nd(apply_transition(pre_mem, es->transition),
                                       lmn_rule_get_name(es->transition.rule));
      }
      
      dfs_expand(next_state,
                 depth+1,
                 new_state,
                 es->transition,
                 i);
      expanded_state_free(es);
    }
    
    print_successor(new_state);
    expanded_free(el);
  }
}

/*
 * 状態を展開する
 * 引数として与えられた膜と、その膜に所属する全てのアクティブ膜に対して
 * ルール適用検査を行う
 * 子膜からルール適用を行っていく
 */
/* must_be_activatedはこの膜がstableである可能性がなくなったときにTRUEを代入する
 * 子膜と自身のルール適応テストが終了したときFALSEならこの膜はstableである
 */
static BOOL expand_inner(LmnMembrane *cur_mem, BOOL *must_be_activated) {
  BOOL ret_flag = FALSE;

  for (; cur_mem; cur_mem = cur_mem->next) {
    BOOL temp_must_be_activated = FALSE;
    unsigned int before_num = expanded_num(expanded);

    /* 代表子膜に対して再帰する */
    if (expand_inner(cur_mem->child_head, &temp_must_be_activated)) { 
      ret_flag = TRUE;
    }

    if (cur_mem->is_activated &&
        react_all_rulesets(cur_mem, &temp_must_be_activated)) {
      ret_flag = TRUE;
    }

    if (expanded_num(expanded) == before_num) {
      cur_mem->is_activated = FALSE;
    }

  }
  return ret_flag;
}

static ExpandedList expand2(LmnMembrane *cur_mem)
{
  BOOL dummy = FALSE;
  ExpandedList bak = expanded;
  ExpandedList exp2;
  
  global_root = cur_mem; /* グローバルルート膜を大域変数に登録する */
  
  exp2 = expanded = vec_make(32);
  expand_inner(cur_mem, &dummy);
  expanded = bak;
  return exp2;
}

/* 本膜の全ルールセットを適用する */
/* must_be_activated_right_underはその膜直下においてルールが適応され、
 * その膜がstableである可能性がなくなった場合にTRUEを代入する
 * 子膜でルールが反応する場合もあるため、FALSEであっても直ちにこの膜がstableであるとは言えない
 * 戻り値をそのまま見るとシステムルールセットの反応を見逃すため使えない
 */
BOOL react_all_rulesets(LmnMembrane *cur_mem, BOOL *must_be_activated_right_under) {
  unsigned int i;
  struct Vector rulesets = cur_mem->rulesets; /* 本膜のルールセットの集合 */
  BOOL temp_must_be_activated = TRUE;

  mc_flags.system_rule_proceeded = FALSE;
  for (i = 0; i < vec_num(&rulesets); i++) {
    LmnRuleSet ruleset = (LmnRuleSet)vec_get(&rulesets, i); /* ルールセット */
/*     printf("react_ruleset in all: "); lmn_dump_mem(cur_mem); */
    react_ruleset(cur_mem, ruleset); /* return FALSE */
  }
  if (!mc_flags.system_rule_proceeded) { /* 通常のルールセットが適用できなかった場合 */
    /* システムルールセットの適用 */
    if (!react_ruleset(cur_mem, system_ruleset)) {
      /* 本膜のルールセット適用検査が（システムルールセット含めて）全て失敗した場合 */
      temp_must_be_activated = FALSE;
    }
  }

  if(temp_must_be_activated){
    *must_be_activated_right_under = TRUE;
  }
  return mc_flags.system_rule_proceeded;
}

unsigned long state_id(McState s)
{
  return (unsigned long)s;
}
